$\forall$${\it the\_w}$:World, $i$:Id, $t$:$\mathbb{N}$, $x$:Id. s($i$;$t$).$x$ $\in$ vartype($i$;$x$)